Nuprl Lemma : minus_thru_mul
12,41
postcript
pdf
a
,
b
:
. (-(
a
*
b
)) = ((-
a
) *
b
)
latex
ProofTree
Definitions
t
T
,
x
:
A
.
B
(
x
)
origin
a, b:
. (-(a * b)) = ((-a) * b)
a, b:. (-(a * b)) = ((-a) * b)
Tx:A. B(x)